package useless;

import atom.UnaryAtom;
import formula.BinaryFormula;
import formula.UnaryFormula;
import literal.UnaryLiteral;
import proof.ConclusionProof;
import proof.Proof;
import sign.FormulaSign;

import java.util.ArrayList;

public class GFTest {
    public void test1(){
        UnaryFormula z=new UnaryFormula(new UnaryLiteral(new UnaryAtom("z"),false));
        UnaryFormula not_z=new UnaryFormula(new UnaryLiteral(new UnaryAtom("z"),true));
        UnaryFormula j=new UnaryFormula(new UnaryLiteral(new UnaryAtom("j"),false));
        UnaryFormula not_j=new UnaryFormula(new UnaryLiteral(new UnaryAtom("j"),true));
        UnaryFormula u=new UnaryFormula(new UnaryLiteral(new UnaryAtom("u"),false));
        UnaryFormula v=new UnaryFormula(new UnaryLiteral(new UnaryAtom("v"),false));
        UnaryFormula not_v=new UnaryFormula(new UnaryLiteral(new UnaryAtom("v"),true));
        UnaryFormula r=new UnaryFormula(new UnaryLiteral(new UnaryAtom("r"),false));

        BinaryFormula bf1=new BinaryFormula(FormulaSign.ANY,v,r);
        BinaryFormula bf2=new BinaryFormula(FormulaSign.EXIST,not_j,j);
        BinaryFormula bf3=new BinaryFormula(FormulaSign.ANY,not_z,z);

        BinaryFormula bfR1=new BinaryFormula(FormulaSign.ANY,u,z);
        BinaryFormula bfR2=new BinaryFormula(FormulaSign.ANY,r,bfR1);
        BinaryFormula tf1=new BinaryFormula(FormulaSign.EXIST,z,bfR2);
        BinaryFormula bfR3=new BinaryFormula(FormulaSign.ANY,z,u);
        BinaryFormula bfR4=new BinaryFormula(FormulaSign.ANY,u,bfR3);
        BinaryFormula tf2=new BinaryFormula(FormulaSign.EXIST,not_j,bfR4);
        BinaryFormula bfR5=new BinaryFormula(FormulaSign.EXIST,j,not_j);
        BinaryFormula tf3=new BinaryFormula(FormulaSign.ANY,not_v,bfR5);
        BinaryFormula bfR6=new BinaryFormula(FormulaSign.ANY,v,not_j);
        BinaryFormula tf4=new BinaryFormula(FormulaSign.ANY,u,bfR6);

        BinaryFormula conclusion=new BinaryFormula(FormulaSign.ANY,r,not_j);

        ArrayList<Proof> proofs=new ArrayList<>();
        proofs.add(new ConclusionProof(bf1));
        proofs.add(new ConclusionProof(bf2));
        proofs.add(new ConclusionProof(bf3));
        proofs.add(new ConclusionProof(tf1));
        proofs.add(new ConclusionProof(tf2));
        proofs.add(new ConclusionProof(tf3));
        proofs.add(new ConclusionProof(tf4));

        //System.out.println(Solve.solveHelper(proofs,conclusion, new UsedCondition()));


    }
    public static void main(String[] args) {
       GFTest test=new GFTest();
       test.test1();
    }
}
